Cut elimination as error correcting device

Abstract: In mathematical proofs axioms and intermediary results are often represented by their names. It is however undecidable whether such a description corresponds to an underlying proof. This implies that there is sometimes no recursive bound of the complexity of the simplest underlying proof in the complexity of the abstract proof description, i.e. the abstract proof description might be non-recursively simpler. This however does not apply to cut-free proofs, where it is easy to decide,whether there is a corresponding proof and it is easy to reconstruct a most general proof in case there is one. This means that cut elimination on an abstract proof description might be considered as error correcting device. We compare various elimination procedures on abstract proof descriptionsand describe their relation to the first epsilon-theorem.

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/